


\paragraph{Adaptation in Structured Communications}
Binary session types were first introduced in~\cite{DBLP:conf/concur/Honda93,DBLP:conf/esop/HondaVK98}.
They have been the subject of intense research in the last two decades, and 
many developments have followed.
Two notable such developments concern asynchronous communications~(see, e.g.,~\cite{DBLP:conf/forte/KouzapasYH11})
and multiparty communications~(see, e.g.,~\cite{DBLP:conf/popl/HondaYC08}, respectively).
%see~\cite{DBLP:conf/wsfm/Dezani-Ciancaglinid09} for a survey.
To the best of our knowledge, our paper~\cite{DBLP:conf/sac/GiustoP13}
was the first work \done\todo[B44.]{Fixed, pls check} to incorporate constructs for runtime adaptation (or evolvability)  into  
a session process language (either binary or multiparty). 
As stated in the Introduction, the present paper is an extended, revised version of~\cite{DBLP:conf/sac/GiustoP13}.
In particular, in this presentation the operational semantics and typing system of~\cite{DBLP:conf/sac/GiustoP13}
have been much simplified.  Following~\cite{DBLP:conf/ppdp/GarraldaCD06}, the operational semantics in~\cite{DBLP:conf/sac/GiustoP13} was
instrumented with several elements to support static analysis.
For instance, %the language in~\cite{DBLP:conf/sac/GiustoP13} features 
one such elements is
a local association between names and session types; such an association is explicitly tracked by a type annotation in prefixes for session acceptance and request. In contrast, for the sake of clarity, 
the semantics given here relies only on a simple runtime annotation for located processes; the other elements are now subsumed by the (revised) typing discipline. Also, to highlight on the simplicity and novelty of our approach, in this presentation we focus on replicated processes, rather than on recursion (the form of infinite behavior given in~\cite{DBLP:conf/sac/GiustoP13}). This is an issue orthogonal to our approach, as discussed in \S\,\ref{sec:disc}.
%\emph{We need to comment on lack of $\Delta_P$ and centralized interfaces.}\todo[B47.]{Perhaps refer here to the absence of a definition such as $\D_P$, carried over now by type judgments?}. 






After our paper~\cite{DBLP:conf/sac/GiustoP13} appeared, some works have addressed the challenging issue of analyzing runtime adaptation in scenarios of \emph{multiparty} communications, in which protocols involve more than two partners.
In such settings, there is a global specification (or \emph{choreography}) to which all interacting partners, from their local perspectives, should adhere. In the  setting of multiparty session types (see, e.g.,~\cite{DBLP:conf/popl/HondaYC08}), these two visions are described by a global type and by local types, respectively; there is a \emph{projection function} which formally relates the two.
The work~\cite{beat2013} defines both global and local languages for choreographies in which adaptation is represented by generalized forms of the adaptable processes in~\cite{BGPZFMOODS}. It is then fair to say that~\cite{beat2013} defines the foundations for extending the present approach to a multiparty setting.
The recent work~\cite{CDV14} proposes a model of self-adaptation for multiparty sessions. Key technical novelties in this approach are 
\emph{monitors} (obtained via projection of global types) and \emph{adaptation functions}. 
Monitors are coupled to processes and govern their behavior; together with global types, adaptation functions embody the runtime adaptation strategy.
An associated typed system ensures communication safety and progress. 
 \done\todo[A11.]{We have included references and comparisons to recent works on adaptations for multiparty communications.} 

\paragraph{Adaptation and Higher-Order Process Communication}
Our constructs for runtime adaptation %present in our session $\pi$-calculus 
(inherited from~\cite{BGPZFMOODS}) 
can be seen as a particular form of \emph{higher-order} communication (or \emph{process-passing}~\cite{San923}). 
In fact, as explained in \S\;\ref{ss:opsem}, our  notion of runtime adaptation formally relies on the objective \emph{movement} of an adaptation routine to a designated location. 
Session type disciplines for a higher-order $\pi$-calculus have been studied in~\cite{DBLP:conf/tlca/MostrousY07}. 
Besides data and session names, session communications in~\cite{DBLP:conf/tlca/MostrousY07}
may also involve code (i.e., process terms), leading to succinct and flexible protocol descriptions. 
%By relying on elements from the linear $\lambda$-calculus, 
The proposed typing system ensures the disciplined use of mobile code exchanged in communications; 
in particular, to avoid communication errors due to unmatched or uncompleted sessions, typing 
ensures that mobile code containing session endpoints is run exactly once. 
In contrast to the process framework in~\cite{DBLP:conf/tlca/MostrousY07}, our model has a rather implicit higher-order character, for we do not allow process communication within sessions.  
Relating our process language with the model in~\cite{DBLP:conf/tlca/MostrousY07} is a promising topic for future work. 
\done\todo[A12.]{We have contrasted our approach to session types for higher-order pi~\cite{DBLP:conf/tlca/MostrousY07}} %d, structured behavior. %determined by the runtime behavior of the system.
Our constructs for runtime adaptation are also related to \emph{passivation} operators found in 
higher-order process calculi (see, e.g.,~\cite{LengletSS11}). There are significant differences between adaptable processes and passivation; 
in particular, adaptable processes distinguish from calculi 
with passivation in that process update   is defined without assuming constructs for higher-order process communication.
See~\cite[\S9.1]{BGPZFMOODS} for a detailed comparison between adaptable processes and passivation.

As already discussed, % along the paper, 
our approach has been influenced by~\cite{DBLP:conf/ppdp/GarraldaCD06} and our previous work~\cite{BGPZFMOODS}. 
Nevertheless, 
there are several major differences between 
our framework and those works. %~\cite{DBLP:conf/ppdp/GarraldaCD06}.
(i)~Unlike the system in~\cite{DBLP:conf/ppdp/GarraldaCD06}, our framework supports channel passing (delegation).
As delegation is already useful to 
represent forms of dynamic reconfiguration, its interplay with update actions is very appealing (cf. the example in \S\,\ref{ss:behdist}).
%\jp{this is no longer useful} 
(ii)~We have extended typing
judgments in~\cite{DBLP:conf/ppdp/GarraldaCD06} with \emph{interfaces} $\INT$, which are % of processes.
central to characterize located processes which can be safely updated. 
%with its two zones, $\Delta_l$ and $\Delta_u$. % and by the necessity of distinguishing between linear and unrestricted actions.
%Another distinctive feature of our approach is the treatment in the typing of the restriction operator. 
%In our setting, communication can happen at any level in the hierarchy of adaptable processes; hence, 
%in order to correctly type the number of active sessions (which, as discussed, is central to enable evolvability steps), the information on used session (e.g. $c:\bot$) cannot be hidden.
%Differences with respect to our previous work~\cite{BGPZFMOODS} are also important.
(iii)~While in~\cite{BGPZFMOODS} adaptable processes are defined for a %(restriction-free) 
fragment of CCS, 
here we consider them within a typed $\pi$-calculus.
(iv)~Adaptation steps in~\cite{BGPZFMOODS} are completely unrestricted. 
%i.e., an update will occur as soon as a located process and an update prefix are able to interact. 
Here we have considered annotated versions of the constructs in~\cite{BGPZFMOODS}:
% Here we have added two elements 
%which serve as a guard for enabling evolvability steps: the number of open sessions in the located processes
%and the interface $\Delta$, present both in the located process and in interacting update processes.
%we think that %our framework enhances the main insights of~\cite{BGPZFMOODS} by 
%they allow to represent evolvable, concurrent systems in a more realistic way, as
%taking the idea of adaptable process to a much more realistic setting, in which 
they offer a more realistic account of update actions, as they are supported 
by runtime conditions based on session types.


\paragraph{Runtime Adaptation} Recently, there has been an increasing interest in %proper definitions of
the specification and verification of autonomic and (self-)adaptive computer systems. 
As a result, several definitions and characterizations of (self-)adaptation have been put forward: 
they reflect the different perspectives and approaches of the several research communities  interested in this class of systems. 
In the Introduction, we have stated our vision of runtime adaptation for communication-based systems. Here we then limit to remark that this vision is well-aligned with the conceptual definition of adaptation recently given in~\cite{DBLP:conf/fase/BruniCGLV12}: ``Given a component with a distinguished collection of control data, adaptation is the runtime modification of such control data.'' 
%As remarked in~\cite{BGPZFMOODS}, 
In the case 
of the calculus of adaptable processes, 
\emph{control data} refers to the located processes in which   behavior can be structured.
The same observation applies for the session calculus considered here, noticing that our framework precisely defines the runtime conditions in which adaptation may consistently occur.


\paragraph{Adaptation vs Exceptions and Compensations}

From a high-level perspective, our typed framework can be related to formal models for service-oriented systems
with constructs such as exceptions and compensations (e.g.,~\cite{DBLP:conf/concur/CarboneHY08,DBLP:books/sp/sensoria2011/FerreiraLRVZ11}). 
In particular,~\cite{DBLP:conf/concur/CarboneHY08} develops a typeful approach for \emph{interactional exceptions}
in asynchronous, binary session types. There, services define a default process and an exception handler, and may be influenced by 
a $\mathtt{throw}$ construct used to throw exceptions;
the associated type system ensures consistent dynamic escaping from possibly nested exception scopes in a concerted way.
We find conceptual differences between 
our intended notion of runtime adaptation (described in the Introduction) and
mechanisms for 
exceptions and compensations.
In our view, such mechanisms 
are concerned only with a particular instance of adaptation/evolvabilty scenarios. 
This way, forms of exceptions (e.g., the one in~\cite{DBLP:conf/concur/CarboneHY08}) should typically handle \emph{internal events}
which  arise during the program's execution and may affect its flow of control. 

Similar in several respects to exceptions, constructs for compensations are usually conceived for 
handling events which are often exceptional \emph{and} catastrophic, such as runtime errors.
This is in contrast with runtime adaptation in modern distributed systems, which 
relies on \emph{external} mechanisms tailored to 
handle general exceptional events, not necessarily catastrophic.
%A familiar example of such events are program upgrades, whose execution can be anticipated and incorporated into the program's code for eventual execution. 
As an example, consider elasticity in cloud-based applications, 
i.e., the ability such applications have to acquire/release computing resources based on user demand.
%depending on user activity, they determine how/when to .
%that in peaks of high activity additional computing resources must be acquired.
Although elasticity triggers 
%Such peaks, while triggering 
system adaptation, % of the system architecture, 
it does not represent a catastrophic event; rather, 
it represents an acceptable (yet hard to predict) state of the system.
Due to this conceptual difference, 
we do not have a clear perspective as to how 
formally relate our approach with 
known models of exceptions/compensations.

%\todo{
Somewhat related to our approach is the work~\cite{DBLP:conf/aplas/AndersonR12}, 
where dynamic runtime update for message passing programs with queues is studied, 
and 
a form of consistency for updates over threads is ensured using 
multiparty session types.
As in our setting,
the notion of update in~\cite{DBLP:conf/aplas/AndersonR12} does not require
  a complete system shutdown, while ensuring that the state of the program remains consistent. 
  However, there are significant 
  conceptual and technical differences. % between our work and~\cite{DBLP:conf/aplas/AndersonR12}. 
First, unlike our approach, in~\cite{DBLP:conf/aplas/AndersonR12} update actions (or adaptation routines)
are defined independently and externally from the program's syntax. 
Second,  here we have considered synchronous communication, 
whereas in~\cite{DBLP:conf/aplas/AndersonR12} an asynchronous thread model with queues is used.
Third, while we have analyzed updates for a language endowed with  binary session types, 
in~\cite{DBLP:conf/aplas/AndersonR12} the need for reaching agreements on multiple threads leads to the use of multiparty session 
types to ensure consistent updates.




\paragraph{Adaptation in Other Settings}
It is instructive to note that approaches similar to ours can also be found in the sequential formalisms for reasoning at lower levels of abstraction. For instance, in~\cite{DBLP:journals/toplas/StoyleHBSN07} the authors introduce dynamic updates to C-like languages, with a focus on runtime update of functions and type declarations. 
They show that dynamic updates are type-safe (consistent) as it cannot happen that different parts of the program expect
different representations of a type. Although the aim is similar, 
it is difficult to establish more precise comparisons, for our interest is in high-level reasoning for communicating programs with precise protocol descriptions.
%clearly, the setting is completely different as moving from a sequential to a concurrent scenario changes considerably the techniques and the problems to be solved.
%}
 In~\cite{DBLP:conf/amast/BrogiCP04} the authors also investigate behavioral types for adaptation, but 
 in the different setting of component-based systems.
Their notion of runtime adaptation %  \todo{different how?} 
relies on a notion of interface which describes the 
behavior of each component. These interfaces are to be used to implement inter-component communication. 
As it could that composition might not work because of  interface mismatching, 
the authors introduce the notion of  \emph{adaptors}, i.e., a software piece that  acts as mediator between two communicating components. It is interesting to notice that a similar mediator behavior could be implemented in our setting, as described in \S\,\ref{ss:behdist}.
%}



%\newpage
%\jp{Other related stuff: \cite{DBLP:conf/aplas/AndersonR12}, possibly also related: \cite{DBLP:conf/isola/LaneseM10,Ivan-Adaptive_C:2013}}
\section{Concluding Remarks}\label{sec:conc}
A main motivation for our work is the observation that while 
paradigms such as service-oriented computing are increasingly popular among practitioners, % software architects and programmers,
formal  models  based on them---such
%core programming calculi based on them---such
as analysis techniques based on session types---fail to capture  
distinctive aspects of such par\-a\-digms.
Here we have  addressed, for the first time, one of such aspects\done\todo[B46.]{We do not like the singular form.}, namely \emph{runtime adaptation}. 
In our view, it
%Here we have addressed one such aspects, runtime adaptation, 
represents an increasingly important concern when analyzing the behavior of communicating systems in 
%, which is intimately related to the fact that service oriented systemsare increasingly being deployed in very highly 
open, context-aware computing infrastructures.

%In this paper w
We have proposed a  framework for
%alternative \todo{approach?} for 
%specifying and 
reasoning about  runtime ad\-ap\-ta\-tion in the context of structured communications
described by session types.
Amalgamating a static analysis technique for correct communications (session types) 
with a novel, inherently dynamic form of interaction (runtime adaptation actions on located processes) is challenging, for 
it requires balancing two different (but equally important) concerns in modern interacting systems. 
In our approach, we %investigated 
are concerned with\done\todo[B45.]{Fixed, pls check}
a session type discipline for an
extended $\pi$-calculus, in which channel mobility (delegation) is enhanced 
with the possibility of performing sophisticated update actions on located processes.
We purposefully aimed at integrating existing, well-studied lines of work: we expect this to be beneficial  for the 
enhancement of other known session type disciplines with adaptation concerns. 
In particular, we built upon our previous work on  
process abstractions for evolvability~\cite{BGPZFMOODS} and
on session types for mobile calculi~\cite{DBLP:conf/ppdp/GarraldaCD06}, relying also on 
a modern account of binary session types~\cite{DBLP:journals/entcs/YoshidaV07}.
In addition to runtime correctness (safety), our typing discipline
ensures consistency: this guarantees that communication behavior (as declared by types) is not disrupted by potential update actions.

%It is aimed at supporting the analysis of service-oriented applications/systems.

There are several avenues for future developments. In ongoing work, we are exploring the use of a 
\emph{typecase} operator (similar to the one proposed in~\cite{DBLP:conf/forte/KouzapasYH11}) to support the runtime adaptation of processes with running sessions. As detailed in \S\,\ref{sec:disc}, this is a challenging issue, for it requires having a uniform treatment of process behavior and the current state of sessions. 
Also, we intend to continue the study of runtime adaptation in a multiparty setting, developing further the approach recently introduced in~\cite{beat2013}.
Furthermore, we plan to investigate 
the interplay of runtime adaptation with
issues such as deadlock-freedom/progress~\cite{DBLP:conf/tgc/Dezani-CiancaglinidY07,DBLP:journals/corr/abs-1010-5566} and  properties related to security, such as access control and information flow~\cite{DBLP:conf/concur/CapecchiCDR10}. 
%In fact, a formal connection between runtime adaptation and security remains to be explored, for runtime errors and security leaks could be p
%which are also important and challenging. %---we plan to look into these in the future. 
%Nevertheless, we believe 
%our work already contributes to the understanding of 
%%that a major contribution of our paper %is novel, as it  is to address 
%issues which, to our knowledge, have not yet  been explored in the realm of 
%session-typed %interacting 
%processes. 




%Our proposal, we believe, combines the most interesting aspects of these previous works in the context of the unexplored setting of evolvable session-typed processes. 
%\newpage
%
%As future work, we plan to investigate stronger notions of correctness for our adaptable, session-typed processes, in particular deadlock-freedom.
%Also, following~\cite{DBLP:journals/acta/GayH05} and the discussion in Sect.\ref{sec:int}, 
%we would like to integrate subtyping into our type system,
%and to obtain algorithmic characterizations
%of notions such as type duality and interface compatibility. 
%This work is an initial 
%step towards a theory of interaction
%in which processes---endowed with behavioral disciplines expressed as types---may dynamically evolve at runtime. 




% . \\%ways of enabling evolvability steps. \\
%-As future work, we plan to investigate stronger notions of correctness for adaptable, session-typed processes, and 
%to develop a formal treatment of subtyping and interface compatibility, along the discussion in Sect.\ref{sec:int}. \\%ways of enabling evolvability steps. \\



\paragraph{Acknowledgments}
%We thank 
%Ant\'{o}nio Ravara,
%Fabrizio Montesi, 
% and
%the SAC'13 and PLACES'13 
We thank the anonymous reviewers for their  detailed remarks. 
This work was 
partially 
supported by the French project
%ANR-11-INSE-0007- REVER and
ANR BLAN 0307 01 - SYNBIOTIC, as well as 
by the 
%Funda\c{c}\~{a}o para a Ci\^{e}ncia e a Tecnologia (
Portuguese Foundation for Science and Technology (FCT) %) 
%through the Carnegie Mellon Portugal Program (grant INTERFACES NGN-44 / 2009) and 
grants  SFRH\;/\;BPD\;/\;84067\;/\;2012
and CITI.
 
%We thank the anonymous reviewers for their useful comments.


